(declare-const v0 Bool)
(declare-const i0 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i12 Int)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const i17 Int)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(push)
(assert (forall ((q0 Int) (q1 Bool)) (=> (or v1 v0 q1 (distinct v1 (<= 90 66) v3 v2 (<= 90 66) v1 (<= 90 66) v1 (<= 90 66))) (> q0 55))))
(declare-const v4 Bool)
(push)
(declare-const v5 Bool)
(declare-const v6 Bool)
(push)
(declare-const v7 Bool)
(declare-const i20 Int)
(declare-const v8 Bool)
(push)
(declare-const i21 Int)
(assert (forall ((q2 Bool) (q3 Int) (q4 Bool) (q5 Bool)) (=> (distinct i16 q3) (not v7))))
(declare-const i22 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(assert (exists ((q6 Bool) (q7 Int) (q8 Bool) (q9 Bool)) (distinct v1 (<= 90 66) v3 v2 (<= 90 66) v1 (<= 90 66) v1 (<= 90 66))))
(declare-const v11 Bool)
(declare-const v12 Bool)
(assert (exists ((q10 Bool) (q11 Int)) (=> (and q10 q10 q10 q10 (or v1 v0 v6 (>= (- (- i0) i4) 676) v0) (= (- (- (- i0) i4) i17 830 i9 i8) i21) v6 (= i6 i6) (= i9 830)) (> q11 q11))))
(push)
(assert (forall ((q12 Bool) (q13 Bool)) (not (or (= i6 i6) q13 q13 q13 q13 q13 q12))))
(declare-const i23 Int)
(declare-const v13 Bool)
(declare-const i24 Int)
(pop)
(declare-const v14 Bool)
(declare-const i25 Int)
(declare-const v15 Bool)
(assert (forall ((q14 Bool) (q15 Bool)) (not (distinct (or v1 (distinct i7 (- (- i0) i4)) v4 (>= i3 55) (= (>= 44 38) v0 v3 (<= 90 66) v1 (distinct v1 (<= 90 66) v3 v2 (<= 90 66) v1 (<= 90 66) v1 (<= 90 66)) (>= 44 38) v2) v6 (= i6 i6)) q14 q15 v0 q14 q14 q15 (not (= (- (- (- i0) i4) i17 830 i9 i8) i21)) v9 v3))))
(declare-const v16 Bool)
(push)
(push)
(declare-const v17 Bool)
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(assert (=> (or (= i9 830) (= i9 830) (= i9 830)) (or (= i9 830) (= i9 830) (= i9 830))))
(assert (or (or (= i9 830) (= i9 830) (= i9 830)) (or (= i9 830) (= i9 830) (= i9 830))))
(check-sat)
(assert (or (= i9 830) (= i9 830) (= i9 830)))
(check-sat)
